Nuprl Lemma : ma-empty-feasible
11,40
postcript
pdf
Feasible()
latex
Definitions
False
,
Id
,
(
x
l
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
Knd
,
IdLnk
,
x
:
A
B
(
x
)
,
b
,
x
dom(
f
)
,
f
(
x
)?
z
,
b
dom(
M
.prob)
,
a
in dom(
M
.pre)
,
x
dom(
f
).
v
=
f
(
x
)
P
(
x
;
v
)
,
M
.da(
a
)
,
ma-prob(
M
;
b
)
,
ma-prob-da-dom(
M
;
b
)
,
ma-frame-compat(
A
;
B
)
,
mk-ma
,
,
ma-prob-da(
M
)
,
Feasible(
M
)
,
origin
l)
Q
x:A. B(x)
B(x)
b dom(f) dom(M.prob)xdom(f). v=f(x) P(x;v)
l) Qx:A. B(x) B(x)b dom(f) dom(M.prob)xdom(f). v=f(x) P(x;v)